Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

f1 -> g1
f1 -> g2
f2 -> g1
f2 -> g2
g1 -> h1
g1 -> h2
g2 -> h1
g2 -> h2
h1 -> i
h2 -> i
e15(h1, h2, x, y, z) -> e25(x, x, y, z, z)
e15(x1, x1, x, y, z) -> e54(x1, x, y, z)
e25(f1, x, y, z, f2) -> e311(x, y, x, y, y, z, y, z, x, y, z)
e25(x, x, y, z, z) -> e63(x, y, z)
e25(i, x, y, z, i) -> e63(x, y, z)
e311(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> e411(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
e311(x, y, x, y, y, z, y, z, x, y, z) -> e63(x, y, z)
e411(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> e15(x1, x1, x, y, z)
e411(i, x1, i, x1, i, x1, i, x1, x, y, z) -> e54(x1, x, y, z)
e411(x, x, x, x, x, x, x, x, x, x, x) -> e63(x, x, x)
e54(i, x, y, z) -> e63(x, y, z)

Q is empty.


QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f1 -> g1
f1 -> g2
f2 -> g1
f2 -> g2
g1 -> h1
g1 -> h2
g2 -> h1
g2 -> h2
h1 -> i
h2 -> i
e15(h1, h2, x, y, z) -> e25(x, x, y, z, z)
e15(x1, x1, x, y, z) -> e54(x1, x, y, z)
e25(f1, x, y, z, f2) -> e311(x, y, x, y, y, z, y, z, x, y, z)
e25(x, x, y, z, z) -> e63(x, y, z)
e25(i, x, y, z, i) -> e63(x, y, z)
e311(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> e411(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
e311(x, y, x, y, y, z, y, z, x, y, z) -> e63(x, y, z)
e411(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> e15(x1, x1, x, y, z)
e411(i, x1, i, x1, i, x1, i, x1, x, y, z) -> e54(x1, x, y, z)
e411(x, x, x, x, x, x, x, x, x, x, x) -> e63(x, x, x)
e54(i, x, y, z) -> e63(x, y, z)

Q is empty.

Q DP problem:
The TRS P consists of the following rules:

F1 -> G2
F2 -> G1
E25(f1, x, y, z, f2) -> E311(x, y, x, y, y, z, y, z, x, y, z)
G1 -> H2
G2 -> H1
E15(x1, x1, x, y, z) -> E54(x1, x, y, z)
E15(h1, h2, x, y, z) -> E25(x, x, y, z, z)
G1 -> H1
F2 -> G2
G2 -> H2
E311(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> E411(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
E411(i, x1, i, x1, i, x1, i, x1, x, y, z) -> E54(x1, x, y, z)
F1 -> G1
E411(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> E15(x1, x1, x, y, z)

The TRS R consists of the following rules:

f1 -> g1
f1 -> g2
f2 -> g1
f2 -> g2
g1 -> h1
g1 -> h2
g2 -> h1
g2 -> h2
h1 -> i
h2 -> i
e15(h1, h2, x, y, z) -> e25(x, x, y, z, z)
e15(x1, x1, x, y, z) -> e54(x1, x, y, z)
e25(f1, x, y, z, f2) -> e311(x, y, x, y, y, z, y, z, x, y, z)
e25(x, x, y, z, z) -> e63(x, y, z)
e25(i, x, y, z, i) -> e63(x, y, z)
e311(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> e411(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
e311(x, y, x, y, y, z, y, z, x, y, z) -> e63(x, y, z)
e411(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> e15(x1, x1, x, y, z)
e411(i, x1, i, x1, i, x1, i, x1, x, y, z) -> e54(x1, x, y, z)
e411(x, x, x, x, x, x, x, x, x, x, x) -> e63(x, x, x)
e54(i, x, y, z) -> e63(x, y, z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

F1 -> G2
F2 -> G1
E25(f1, x, y, z, f2) -> E311(x, y, x, y, y, z, y, z, x, y, z)
G1 -> H2
G2 -> H1
E15(x1, x1, x, y, z) -> E54(x1, x, y, z)
E15(h1, h2, x, y, z) -> E25(x, x, y, z, z)
G1 -> H1
F2 -> G2
G2 -> H2
E311(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> E411(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
E411(i, x1, i, x1, i, x1, i, x1, x, y, z) -> E54(x1, x, y, z)
F1 -> G1
E411(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> E15(x1, x1, x, y, z)

The TRS R consists of the following rules:

f1 -> g1
f1 -> g2
f2 -> g1
f2 -> g2
g1 -> h1
g1 -> h2
g2 -> h1
g2 -> h2
h1 -> i
h2 -> i
e15(h1, h2, x, y, z) -> e25(x, x, y, z, z)
e15(x1, x1, x, y, z) -> e54(x1, x, y, z)
e25(f1, x, y, z, f2) -> e311(x, y, x, y, y, z, y, z, x, y, z)
e25(x, x, y, z, z) -> e63(x, y, z)
e25(i, x, y, z, i) -> e63(x, y, z)
e311(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> e411(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
e311(x, y, x, y, y, z, y, z, x, y, z) -> e63(x, y, z)
e411(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> e15(x1, x1, x, y, z)
e411(i, x1, i, x1, i, x1, i, x1, x, y, z) -> e54(x1, x, y, z)
e411(x, x, x, x, x, x, x, x, x, x, x) -> e63(x, x, x)
e54(i, x, y, z) -> e63(x, y, z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 1 SCC with 10 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
QDP

Q DP problem:
The TRS P consists of the following rules:

E15(h1, h2, x, y, z) -> E25(x, x, y, z, z)
E311(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> E411(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
E411(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> E15(x1, x1, x, y, z)
E25(f1, x, y, z, f2) -> E311(x, y, x, y, y, z, y, z, x, y, z)

The TRS R consists of the following rules:

f1 -> g1
f1 -> g2
f2 -> g1
f2 -> g2
g1 -> h1
g1 -> h2
g2 -> h1
g2 -> h2
h1 -> i
h2 -> i
e15(h1, h2, x, y, z) -> e25(x, x, y, z, z)
e15(x1, x1, x, y, z) -> e54(x1, x, y, z)
e25(f1, x, y, z, f2) -> e311(x, y, x, y, y, z, y, z, x, y, z)
e25(x, x, y, z, z) -> e63(x, y, z)
e25(i, x, y, z, i) -> e63(x, y, z)
e311(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z) -> e411(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z)
e311(x, y, x, y, y, z, y, z, x, y, z) -> e63(x, y, z)
e411(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z) -> e15(x1, x1, x, y, z)
e411(i, x1, i, x1, i, x1, i, x1, x, y, z) -> e54(x1, x, y, z)
e411(x, x, x, x, x, x, x, x, x, x, x) -> e63(x, x, x)
e54(i, x, y, z) -> e63(x, y, z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.